R:Realizer, z, i:Id. R-occurs(R;i;z)   

latex

Definitions

t  T, x:A. B(x), a = b, p  q, false, IdDeq, Id, deq-member(eq;x;L), Type, x.A(x), x. t(x), a:A fp B(a), Top, x:AB(x), x  dom(f), source(l), p  q, Knd, type List, IdLnk, Prop, State(ds), DeclaredType(ds;x), x:AB(x), Realizer, , x,y,z. t(x;y;z), x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), es realizer ind, es realizer ind Rrframe compseq tag def, R-occurs(R;i;z), es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, left+right, s = t, Unit, rec(x.A(x))

Lemmas

unit wf, es realizer ind wf, bool wf, es realizer wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, bor wf, lsrc wf, fpf-dom wf, fpf-trivial-subtype-top, deq-member wf, Id wf, id-deq wf, bfalse wf, band wf, eq id wf